Nuprl Lemma : swap_wf
4,23
postcript
pdf
T
:Type,
L
:
T
List,
i
,
j
:
||
L
||. swap(
L
;
i
;
j
)
T
List
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
{
i
..
j
}
,
A
B
,
P
&
Q
,
i
j
<
k
,
P
Q
,
False
,
A
,
,
(
i
,
j
)
,
(
L
o
f
)
,
swap(
L
;
i
;
j
)
Lemmas
permute
list
wf
,
flip
wf
,
le
wf
,
int
seg
wf
,
length
wf1
origin
T:Type, L:T List, i, j:
||L||. swap(L;i;j) 
T List T:Type, L:T List, i, j:||L||. swap(L;i;j) T List Tx:A. B(x)
}
B j < k
Q
A